active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
MARK(a) → ACTIVE(a)
MARK(f(X1, X2)) → MARK(X1)
F(active(X1), X2) → F(X1, X2)
F(X1, mark(X2)) → F(X1, X2)
MARK(f(X1, X2)) → F(mark(X1), X2)
ACTIVE(b) → MARK(a)
ACTIVE(f(X, X)) → F(a, b)
F(X1, active(X2)) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
MARK(b) → ACTIVE(b)
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
ACTIVE(f(X, X)) → MARK(f(a, b))
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MARK(a) → ACTIVE(a)
MARK(f(X1, X2)) → MARK(X1)
F(active(X1), X2) → F(X1, X2)
F(X1, mark(X2)) → F(X1, X2)
MARK(f(X1, X2)) → F(mark(X1), X2)
ACTIVE(b) → MARK(a)
ACTIVE(f(X, X)) → F(a, b)
F(X1, active(X2)) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
MARK(b) → ACTIVE(b)
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
ACTIVE(f(X, X)) → MARK(f(a, b))
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
F(active(X1), X2) → F(X1, X2)
F(X1, mark(X2)) → F(X1, X2)
F(X1, active(X2)) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(active(X1), X2) → F(X1, X2)
F(mark(X1), X2) → F(X1, X2)
Used ordering: Polynomial interpretation [25,35]:
F(X1, mark(X2)) → F(X1, X2)
F(X1, active(X2)) → F(X1, X2)
The value of delta used in the strict ordering is 1/16.
POL(active(x1)) = 1/4 + (2)x_1
POL(mark(x1)) = 1/4 + (4)x_1
POL(F(x1, x2)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(X1, mark(X2)) → F(X1, X2)
F(X1, active(X2)) → F(X1, X2)
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(X1, active(X2)) → F(X1, X2)
Used ordering: Polynomial interpretation [25,35]:
F(X1, mark(X2)) → F(X1, X2)
The value of delta used in the strict ordering is 8.
POL(active(x1)) = 4 + (2)x_1
POL(mark(x1)) = (2)x_1
POL(F(x1, x2)) = (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
F(X1, mark(X2)) → F(X1, X2)
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(X1, mark(X2)) → F(X1, X2)
The value of delta used in the strict ordering is 1/16.
POL(mark(x1)) = 1/4 + (2)x_1
POL(F(x1, x2)) = (1/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
MARK(f(X1, X2)) → MARK(X1)
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
ACTIVE(f(X, X)) → MARK(f(a, b))
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(f(X1, X2)) → MARK(X1)
Used ordering: Polynomial interpretation [25,35]:
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
ACTIVE(f(X, X)) → MARK(f(a, b))
The value of delta used in the strict ordering is 1/2.
POL(active(x1)) = 0
POL(MARK(x1)) = (1/4)x_1
POL(a) = 0
POL(f(x1, x2)) = 2 + (2)x_1
POL(mark(x1)) = 0
POL(b) = 0
POL(ACTIVE(x1)) = 1/2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
MARK(f(X1, X2)) → ACTIVE(f(mark(X1), X2))
ACTIVE(f(X, X)) → MARK(f(a, b))
active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
mark(f(X1, X2)) → active(f(mark(X1), X2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2) → f(X1, X2)
f(X1, mark(X2)) → f(X1, X2)
f(active(X1), X2) → f(X1, X2)
f(X1, active(X2)) → f(X1, X2)